fix(lol/abi): make the lol-abi Idris package typecheck#389
Merged
Conversation
The lol-abi.ipkg package did not build. All failures were in
estate-authored (MPL-2.0) modules; fixed without any believe_me or holes.
Layout.idr:
- Every MkStructLayout left its erased `aligned : Divides alignment
totalSize` auto-implicit to proof search, which cannot guess the
quotient k. Supplied it explicitly per layout via
{aligned = DivideBy k Refl} (32=4*8, 24=3*8, 56=7*8, 40=5*8, 16=4*4).
- paddingFor used `-` on Nat, resolving to a nonexistent `Neg Nat`;
switched to truncating `minus`.
- Removed the unused `alignUpCorrect` lemma: its `Refl` body asserted
`n = (n `div` a) * a`, which only holds definitionally for concrete
args, so it never typechecked. A correct general proof needs the
division theorem (absent from Idris2 base); the divisibility the
concrete layouts need is discharged per-layout by the explicit
DivideBy witnesses. Documented as future work.
I18nStore.idr:
- extractLanguage used Data.List1.split (wants a List) on a String;
switched to Data.String.split.
- LookupError used `data X = .. | ..` with per-constructor `|||` doc
comments (only valid in GADT form); converted to
`data LookupError : Type where`.
- The CorrectStore interface ended with a dangling `|||` doc comment
(no method after it), breaking the block's scope so the following
top-level `data LookupError` failed to register; demoted to a plain
comment.
`idris2 --build lol-abi.ipkg` now exits 0 (pre-existing shadowing
warnings only).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019awZjBD1qx61tvmEuEKNpn
🔍 Hypatia Security ScanFindings: 148 issues detected
View findings[
{
"reason": "Issue in scorecard.yml",
"type": "missing_workflow",
"file": "scorecard.yml",
"action": "create",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in scorecard-enforcer.yml",
"type": "scorecard_publish_with_run_step",
"file": "scorecard-enforcer.yml",
"action": "split_scorecard_publish_job",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in instant-sync.yml",
"type": "secret_action_without_presence_gate",
"file": "instant-sync.yml",
"action": "peter-evans/repository-dispatch",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Required file missing (condition: public_repo)",
"type": "missing_requirement",
"file": ".github/workflows/scorecard.yml",
"action": "create",
"rule_module": "cicd_rules",
"severity": "high"
},
{
"reason": "TypeScript file detected -- banned language",
"type": "banned_language_file",
"file": "/home/runner/work/standards/standards/scripts/check-ts-allowlist.ts",
"action": "flag",
"rule_module": "cicd_rules",
"severity": "critical"
},
{
"reason": "Agda postulate assumes without proof -- potential soundness hole (4 occurrences, CWE-704)",
"type": "agda_postulate",
"file": "/home/runner/work/standards/standards/lol/proofs/theories/information_theory.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "innerHTML assignment -- XSS risk, use textContent or SafeDOM (5 occurrences, CWE-79)",
"type": "js_innerhtml",
"file": "/home/runner/work/standards/standards/avow-protocol/public/demo.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "innerHTML assignment -- XSS risk, use textContent or SafeDOM (1 occurrences, CWE-79)",
"type": "js_innerhtml",
"file": "/home/runner/work/standards/standards/axel-protocol/src/Tea.res.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "Wildcard CORS -- restrict to specific origins or use env var (1 occurrences, CWE-942)",
"type": "js_wildcard_cors",
"file": "/home/runner/work/standards/standards/consent-aware-http/examples/reference-implementations/deno/aibdp_middleware.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "HTTP URL in Nickel config -- must use HTTPS (1 occurrences, CWE-319)",
"type": "ncl_http_url",
"file": "/home/runner/work/standards/standards/k9-svc/register.ncl",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
`scripts/build-registry.sh --check` (the "Registry + topology in sync" gate) failed on this PR: the recorded source_hash for the consent-aware-http/ spec was stale. This is a PRE-EXISTING drift on the branch, unrelated to the lol/abi Idris fix (lol/ is not a registered spec home). Regenerated via the sanctioned generator `bash scripts/build-registry.sh` — the file MUST NOT be hand-edited. Only the consent-aware-http/ source_hash changed; TOPOLOGY.md was already in sync. This is an index content-hash update, not a license or content change to the carve-out repo. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019awZjBD1qx61tvmEuEKNpn
🔍 Hypatia Security ScanFindings: 148 issues detected
View findings[
{
"reason": "Issue in scorecard.yml",
"type": "missing_workflow",
"file": "scorecard.yml",
"action": "create",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in scorecard-enforcer.yml",
"type": "scorecard_publish_with_run_step",
"file": "scorecard-enforcer.yml",
"action": "split_scorecard_publish_job",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in instant-sync.yml",
"type": "secret_action_without_presence_gate",
"file": "instant-sync.yml",
"action": "peter-evans/repository-dispatch",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Required file missing (condition: public_repo)",
"type": "missing_requirement",
"file": ".github/workflows/scorecard.yml",
"action": "create",
"rule_module": "cicd_rules",
"severity": "high"
},
{
"reason": "TypeScript file detected -- banned language",
"type": "banned_language_file",
"file": "/home/runner/work/standards/standards/scripts/check-ts-allowlist.ts",
"action": "flag",
"rule_module": "cicd_rules",
"severity": "critical"
},
{
"reason": "Agda postulate assumes without proof -- potential soundness hole (4 occurrences, CWE-704)",
"type": "agda_postulate",
"file": "/home/runner/work/standards/standards/lol/proofs/theories/information_theory.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "innerHTML assignment -- XSS risk, use textContent or SafeDOM (5 occurrences, CWE-79)",
"type": "js_innerhtml",
"file": "/home/runner/work/standards/standards/avow-protocol/public/demo.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "innerHTML assignment -- XSS risk, use textContent or SafeDOM (1 occurrences, CWE-79)",
"type": "js_innerhtml",
"file": "/home/runner/work/standards/standards/axel-protocol/src/Tea.res.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "Wildcard CORS -- restrict to specific origins or use env var (1 occurrences, CWE-942)",
"type": "js_wildcard_cors",
"file": "/home/runner/work/standards/standards/consent-aware-http/examples/reference-implementations/deno/aibdp_middleware.js",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "HTTP URL in Nickel config -- must use HTTPS (1 occurrences, CWE-319)",
"type": "ncl_http_url",
"file": "/home/runner/work/standards/standards/k9-svc/register.ncl",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
hyperpolymath
added a commit
that referenced
this pull request
Jun 18, 2026
## Summary The **standards RSR compliance pass** — continuation of the standards end-to-end (the Idris ABI fix landed separately in #389). Takes the standards self-audit from **58.46% → 85.92% (🥉 BRONZE)**. ### 1. Real gaps (additive) — `feat(rsr)` - `.well-known/security.txt` (RFC 9116: Contact/Expires/Preferred-Languages → GitHub Security Advisory + SECURITY.md) - `.well-known/ai.txt` (AI usage/training policy; summary of the estate bot-exclusion registry + `0-ai-gatekeeper-protocol`) - `.well-known/humans.txt` (humanstxt.org attribution) - Justfile `validate` recipe (registry-check hard-dep + RSR self-audit) ### 2. Audit-script de-brittle — `fix(rsr-audit)` `rsr-audit.sh` was mis-calibrated for this GitHub/`.adoc` estate, failing repos on deliberate, policy-correct choices. De-brittled **format/case only** in the two core helpers + the CI check — **licence content checks untouched**: - credit `.adoc` docs (estate docs policy mandates AsciiDoc), `Justfile` case, bare `LICENSE` - accept GitHub Actions (`.github/workflows/*.y*ml`) as first-class (not just GitLab CI / a hardcoded `ci.yml`) — the estate runs on GitHub; the RSR satellite `CLAUDE.md` itself notes the old GitLab guidance is superseded. Improves scoring for **all 10 estate repos**, not just standards. ## 🔒 Flagged for owner (NOT changed — licence guardrail) `rsr-audit.sh` hardcodes `MIT AND Palimpsest` as the required LICENSE *content* (≈ lines 194/424/430), which contradicts the estate's MPL-2.0-for-sole-owner policy. Updating what licence the standard mandates is an owner decision — left as-is. ## Residual (honest) 3 checks still fail, all content-pattern brittleness for content the estate phrases differently: SECURITY "24 hours" literal (standards has a Response Timeline section), the exact TPCF perimeter strings, and "fork workflow" (standards uses the TPCF perimeter model, not a fork workflow). BRONZE (≥75%) is achieved; these can be de-brittled in a follow-up. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_019awZjBD1qx61tvmEuEKNpn --- _Generated by [Claude Code](https://claude.ai/code/session_019awZjBD1qx61tvmEuEKNpn)_
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
First unit of bringing standards toward proof/RSR compliance: making the
lol-abiIdris package typecheck (it previously did not build at all).lol/is hyperpolymath's port of Ehsaneddin Asgari's 1000Langs; the Idris ABI modules fixed here are estate-authored (MPL-2.0).idris2 --build lol-abi.ipkgnow exits 0 (pre-existing shadowing warnings only). Nobelieve_me, no holes.Layout.idrMkStructLayoutleft its erasedaligned : Divides alignment totalSizeauto-implicit to proof search, which cannot guess the quotientk. Supplied explicitly per layout via{aligned = DivideBy k Refl}(32=4·8, 24=3·8, 56=7·8, 40=5·8, 16=4·4).paddingForused-onNat(resolves to a nonexistentNeg Nat) → truncatingminus.alignUpCorrectlemma: itsReflbody assertedn = (n div a)·a, true only for concrete args. A correct general proof needs the division theorem (absent from Idris2base); the divisibility the real layouts need is discharged per-layout by the explicitDivideBywitnesses. Documented as future work.I18nStore.idrextractLanguageusedData.List1.split(wants aList) on aString→Data.String.split.LookupErroruseddata X = .. | ..with per-constructor|||doc comments (only valid in GADT form) →data LookupError : Type where.CorrectStoreinterface ended with a dangling|||doc comment (no method after it), breaking the block's scope so the following top-leveldata LookupErrorfailed to register → demoted to a plain comment.Flagged for owner (NOT touched — license guardrail)
lol/proofs/theories/information_theory.agdais third-party-attributed (MIT AND LicenseRef-Palimpsest-0.8, © Ehsaneddin Asgari). It has a trivial syntax bug (illegalwhereinsidepostulate), but editing a third-party-attributed file is owner-only — left untouched, flagged.rhodium-standard-repositories/rsr-audit.shhardcodesMIT AND Palimpsestas the required license, contradicting the estate's current MPL-2.0-for-sole-owner policy. Updating what license the standard mandates is owner-only — flagged, not changed. RSR format-brittleness fixes + real gaps (.well-known, Justfilevalidate) will follow on this branch.🤖 Generated with Claude Code
https://claude.ai/code/session_019awZjBD1qx61tvmEuEKNpn
Generated by Claude Code